// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! find mod.rs for centralized documentation
//!
//! This file contains [IrepId] which is the id's used in CBMC.
//! c.f. CBMC source code [src/util/irep_ids.def]
use crate::cbmc_string::InternedString;
use crate::utils::NumUtils;
use num::bigint::{BigInt, BigUint, Sign};

use std::borrow::Cow;

#[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)]
pub enum IrepId {
    /// In addition to the standard enums defined below, CBMC also allows ids to be strings.
    /// For e.g, to store the id of a variable. This enum variant captures those strings.
    FreeformString(InternedString),
    /// An integer, to be encoded as a decimal string
    FreeformInteger(BigInt),
    /// A constant, stored as a bit pattern (negative numbers in 2's complement).
    FreeformBitPattern(BigUint),
    EmptyString,
    Let,
    LetBinding,
    Nil,
    Type,
    Bool,
    CBool,
    ProperBool,
    Signedbv,
    Unsignedbv,
    VerilogSignedbv,
    VerilogUnsignedbv,
    Floatbv,
    Fixedbv,
    X86Extended,
    CSourceLocation,
    CEndLocation,
    CIsPadding,
    CDoNotDump,
    File,
    Line,
    Column,
    Comment,
    Property,
    PropertyClass,
    PropertyId,
    Function,
    MathematicalFunction,
    Code,
    Typecast,
    StaticCast,
    DynamicCast,
    ConstCast,
    ReinterpretCast,
    Index,
    Ptrmember,
    Member,
    MemberName,
    CMemberName,
    Equal,
    Implies,
    And,
    Nand,
    Or,
    Nor,
    Xor,
    Not,
    Bitand,
    Bitor,
    Bitnot,
    Bitxor,
    Bitnand,
    Bitnor,
    Bitxnor,
    Notequal,
    If,
    Symbol,
    NextSymbol,
    NondetSymbol,
    PredicateSymbol,
    PredicateNextSymbol,
    NondetBool,
    Empty,
    SideEffect,
    Statement,
    StatementExpression,
    Value,
    Constant,
    Block,
    Decl,
    Dead,
    Assign,
    AssignDiv,
    AssignMult,
    AssignPlus,
    AssignMinus,
    AssignMod,
    AssignShl,
    AssignShr,
    AssignAshr,
    AssignLshr,
    AssignBitand,
    AssignBitxor,
    AssignBitor,
    Assume,
    Assert,
    Assertion,
    Precondition,
    Postcondition,
    PreconditionInstance,
    Goto,
    GccComputedGoto,
    Ifthenelse,
    Label,
    Break,
    Continue,
    FunctionCall,
    Return,
    Skip,
    Arguments,
    Array,
    Size,
    FrontendPointer,
    Pointer,
    BlockPointer,
    Switch,
    SwitchCase,
    GccSwitchCaseRange,
    For,
    While,
    Dowhile,
    Int,
    Integer,
    Natural,
    Real,
    Rational,
    Complex,
    Signed,
    Unsigned,
    Asm,
    GccAsmInput,
    GccAsmOutput,
    GccAsmClobberedRegister,
    Incomplete,
    IncompleteClass,
    CIncomplete,
    Identifier,
    Name,
    InnerName,
    CppName,
    ComponentCppName,
    CIdClass,
    Declaration,
    DeclarationList,
    Declarator,
    Struct,
    CBitField,
    Union,
    Class,
    MergedType,
    Range,
    From,
    To,
    Module,
    Parameter,
    ComponentName,
    ComponentNumber,
    Tag,
    Default,
    CDefaultValue,
    BaseName,
    CBaseName,
    String,
    CStringConstant,
    StringConstant,
    Width,
    Components,
    Bv,
    F,
    With,
    Trans,
    Throw,
    TryCatch,
    Noexcept,
    CPROVERThrow,
    CPROVERTryCatch,
    CPROVERTryFinally,
    Protection,
    Private,
    Public,
    Protected,
    Virtual,
    Volatile,
    Const,
    Constexpr,
    Inline,
    Forall,
    Exists,
    Repeat,
    Extractbit,
    Extractbits,
    CReference,
    CRvalueReference,
    True,
    False,
    AddressOf,
    Dereference,
    CLvalue,
    CBase,
    Destination,
    Main,
    Expression,
    Allocate,
    CCxxAllocType,
    CppNew,
    CppDelete,
    CppNewArray,
    CppDeleteArray,
    JavaNew,
    JavaNewArray,
    JavaNewArrayData,
    JavaStringLiteral,
    Printf,
    Input,
    Output,
    Nondet,
    NULL,
    Null,
    Nullptr,
    CEnum,
    Enumeration,
    Elements,
    Unknown,
    Uninitialized,
    Invalid,
    CInvalidObject,
    PointerOffset,
    PointerObject,
    IsInvalidPointer,
    IeeeFloatEqual,
    IeeeFloatNotequal,
    Isnan,
    Lambda,
    ArrayComprehension,
    ArrayOf,
    ArrayEqual,
    ArraySet,
    ArrayCopy,
    ArrayList,
    Mod,
    Rem,
    Shr,
    Ashr,
    Lshr,
    Shl,
    Rol,
    Ror,
    Comma,
    Concatenation,
    Infinity,
    ReturnType,
    Typedef,
    TypedefType,
    CTypedef,
    Extern,
    Static,
    Auto,
    Register,
    ThreadLocal,
    Thread,
    CThreadLocal,
    CStaticLifetime,
    Mutable,
    Void,
    Int8,
    Int16,
    Int32,
    Int64,
    Ptr32,
    Ptr64,
    Char,
    Short,
    Long,
    Float,
    Float16,
    Float128,
    Double,
    Byte,
    Boolean,
    LongDouble,
    SignedChar,
    UnsignedChar,
    SignedInt,
    UnsignedInt,
    SignedLongInt,
    UnsignedLongInt,
    SignedShortInt,
    UnsignedShortInt,
    SignedLongLongInt,
    UnsignedLongLongInt,
    SignedInt128,
    UnsignedInt128,
    Case,
    CInlined,
    CHide,
    Hide,
    Abs,
    Sign,
    Access,
    CAccess,
    Postincrement,
    Postdecrement,
    Preincrement,
    Predecrement,
    IntegerBits,
    KnR,
    CKnR,
    ConstraintSelectOne,
    Cond,
    BvLiterals,
    IsFinite,
    Isinf,
    Isnormal,
    Alignof,
    ClangBuiltinConvertvector,
    GccBuiltinVaArg,
    GccBuiltinTypesCompatibleP,
    VaStart,
    GccFloat16,
    GccFloat32,
    GccFloat32x,
    GccFloat64,
    GccFloat64x,
    GccFloat80,
    GccFloat128,
    GccFloat128x,
    GccInt128,
    GccDecimal32,
    GccDecimal64,
    GccDecimal128,
    BuiltinOffsetof,
    Id0,
    Id1,
    Sizeof,
    TypeArg,
    ExprArg,
    ExpressionList,
    InitializerList,
    GccConditionalExpression,
    GccLocalLabel,
    Gcc,
    Msc,
    Typeof,
    Ellipsis,
    Flavor,
    Ge,
    Le,
    Gt,
    Lt,
    Plus,
    Minus,
    UnaryMinus,
    UnaryPlus,
    Mult,
    Div,
    Power,
    FactorialPower,
    CPrettyName,
    CClass,
    CField,
    CInterface,
    DesignatedInitializer,
    Designator,
    MemberDesignator,
    IndexDesignator,
    CConstant,
    CVolatile,
    CRestricted,
    CIdentifier,
    CImplicit,
    CPtr32,
    CPtr64,
    CAtomic,
    Restrict,
    ByteExtractBigEndian,
    ByteExtractLittleEndian,
    ByteUpdateBigEndian,
    ByteUpdateLittleEndian,
    Replication,
    CproverAtomic,
    Atomic,
    AtomicTypeSpecifier,
    AtomicBegin,
    AtomicEnd,
    StartThread,
    EndThread,
    CoverageCriterion,
    Initializer,
    Anonymous,
    CIsAnonymous,
    IsEnumConstant,
    IsInline,
    IsExtern,
    IsSynchronized,
    IsNativeMethod,
    IsVarargsMethod,
    IsGlobal,
    IsThreadLocal,
    IsParameter,
    IsMember,
    IsType,
    IsRegister,
    IsTypedef,
    IsStatic,
    IsTemplate,
    IsStaticAssert,
    IsVirtual,
    CIsVirtual,
    Literal,
    MemberInitializers,
    MemberInitializer,
    MethodQualifier,
    Methods,
    StaticMembers,
    Constructor,
    Destructor,
    Bases,
    Base,
    FromBase,
    Operator,
    Template,
    TemplateClassInstance,
    TemplateFunctionInstance,
    TemplateType,
    TemplateArgs,
    TemplateParameter,
    TemplateParameterSymbolType,
    TemplateParameters,
    CTemplate,
    CTemplateArguments,
    CTemplateCase,
    Typename,
    C,
    Cpp,
    Java,
    DeclBlock,
    DeclType,
    Parameters,
    WcharT,
    Char16T,
    Char32T,
    SizeT,
    SsizeT,
    Mode,
    This,
    CThis,
    ReductionAnd,
    ReductionOr,
    ReductionNand,
    ReductionNor,
    ReductionXor,
    ReductionXnor,
    CZeroInitializer,
    Body,
    TemporaryObject,
    OverflowPlus,
    OverflowMinus,
    OverflowMult,
    OverflowResultPlus,
    OverflowResultMinus,
    OverflowResultMult,
    OverflowUnaryMinus,
    ObjectDescriptor,
    IsDynamicObject,
    DynamicObject,
    CDynamic,
    ObjectSize,
    GoodPointer,
    IntegerAddress,
    IntegerAddressObject,
    NullObject,
    StaticObject,
    StackObject,
    CIsFailedSymbol,
    CFailedSymbol,
    Friend,
    CFriends,
    Explicit,
    StorageSpec,
    MemberSpec,
    MscDeclspec,
    Packed,
    CPacked,
    TransparentUnion,
    CTransparentUnion,
    Aligned,
    CAlignment,
    FrontendVector,
    Vector,
    Abstract,
    FunctionApplication,
    CppDeclarator,
    CppLinkageSpec,
    CppNamespaceSpec,
    CppStorageSpec,
    CppUsing,
    CppDeclaration,
    CppStaticAssert,
    CppMemberSpec,
    CCType,
    Namespace,
    Linkage,
    Decltype,
    CTagOnlyDeclaration,
    StructTag,
    UnionTag,
    CEnumTag,
    VerilogCaseEquality,
    VerilogCaseInequality,
    UserSpecifiedPredicate,
    UserSpecifiedParameterPredicates,
    UserSpecifiedReturnPredicates,
    Unassigned,
    NewObject,
    ComplexReal,
    ComplexImag,
    Imag,
    MscTryExcept,
    MscTryFinally,
    MscLeave,
    MscUuidof,
    MscIfExists,
    MscIfNotExists,
    MscUnderlyingType,
    MscBased,
    Alias,
    PtrObject,
    CCSizeofType,
    ArrayUpdate,
    Update,
    StaticAssert,
    GccAttributeMode,
    BuiltIn,
    ExceptionList,
    ExceptionId,
    PredicatePassiveSymbol,
    CwVaArgTypeof,
    Fence,
    Sync,
    Lwsync,
    Isync,
    WRfence,
    RRfence,
    RWfence,
    WWfence,
    RRcumul,
    RWcumul,
    WWcumul,
    WRcumul,
    GenericSelection,
    GenericAssociations,
    GenericAssociation,
    FloatbvPlus,
    FloatbvMinus,
    FloatbvMult,
    FloatbvDiv,
    FloatbvRem,
    FloatbvTypecast,
    CompoundLiteral,
    CustomBv,
    CustomUnsignedbv,
    CustomSignedbv,
    CustomFixedbv,
    CustomFloatbv,
    CSSASymbol,
    L0,
    L1,
    L2,
    L1ObjectIdentifier,
    AlreadyTypechecked,
    CVaArgType,
    Smt2Symbol,
    Onehot,
    Onehot0,
    Popcount,
    CountLeadingZeros,
    CountTrailingZeros,
    EmptyUnion,
    FunctionType,
    Noreturn,
    CNoreturn,
    Weak,
    IsWeak,
    Used,
    IsUsed,
    CSpecLoopInvariant,
    CSpecRequires,
    CSpecEnsures,
    CSpecAssigns,
    VirtualFunction,
    ElementType,
    WorkingDirectory,
    Section,
    Bswap,
    BitReverse,
    JavaBytecodeIndex,
    JavaInstanceof,
    JavaSuperMethodCall,
    JavaEnumStaticUnwind,
    PushCatch,
    PopCatch,
    ExceptionLandingpad,
    LengthUpperBound,
    CproverAssociateArrayToPointerFunc,
    CproverAssociateLengthToArrayFunc,
    CproverCharLiteralFunc,
    CproverStringLiteralFunc,
    CproverStringCharAtFunc,
    CproverStringCharSetFunc,
    CproverStringCodePointAtFunc,
    CproverStringCodePointBeforeFunc,
    CproverStringCodePointCountFunc,
    CproverStringOffsetByCodePointFunc,
    CproverStringCompareToFunc,
    CproverStringConcatFunc,
    CproverStringConcatCharFunc,
    CproverStringConcatCodePointFunc,
    CproverStringConstrainCharactersFunc,
    CproverStringContainsFunc,
    CproverStringCopyFunc,
    CproverStringDeleteFunc,
    CproverStringDeleteCharAtFunc,
    CproverStringEqualFunc,
    CproverStringEqualsIgnoreCaseFunc,
    CproverStringEmptyStringFunc,
    CproverStringEndswithFunc,
    CproverStringFormatFunc,
    CproverStringIndexOfFunc,
    CproverStringInsertFunc,
    CproverStringIsPrefixFunc,
    CproverStringIsSuffixFunc,
    CproverStringIsEmptyFunc,
    CproverStringLastIndexOfFunc,
    CproverStringLengthFunc,
    CproverStringOfIntFunc,
    CproverStringOfIntHexFunc,
    CproverStringOfLongFunc,
    CproverStringOfFloatFunc,
    CproverStringOfFloatScientificNotationFunc,
    CproverStringOfDoubleFunc,
    CproverStringParseIntFunc,
    CproverStringIsValidIntFunc,
    CproverStringIsValidLongFunc,
    CproverStringReplaceFunc,
    CproverStringSetLengthFunc,
    CproverStringStartswithFunc,
    CproverStringSubstringFunc,
    CproverStringToLowerCaseFunc,
    CproverStringToUpperCaseFunc,
    CproverStringTrimFunc,
    SkipInitialize,
    BasicBlockCoveredLines,
    BasicBlockSourceLines,
    IsNondetNullable,
    ArrayReplace,
    SwitchCaseNumber,
    JavaArrayAccess,
    JavaMemberAccess,
    CJavaGenericParameter,
    CJavaGenericsClassType,
    CJavaImplicitlyGenericClassType,
    CJavaGenericSymbol,
    GenericTypes,
    ImplicitGenericTypes,
    TypeVariables,
    HandleType,
    JavaLambdaMethodHandle,
    JavaLambdaMethodHandleIndex,
    JavaLambdaMethodHandles,
    HavocObject,
    OverflowShl,
    CNoInitializationRequired,
    CNoNondetInitialization,
    OverlayClass,
    OverlayMethod,
    IgnoredMethod,
    IsAnnotation,
    CAnnotations,
    Final,
    BitsPerByte,
    CAbstract,
    Synthetic,
    Interface,
    CMustNotThrow,
    IsInnerClass,
    IsAnonymous,
    OuterClass,
    IsBridgeMethod,
    CIsOperator,
    CNotAccessible,
    COverrideConstantness,
    CBound,
    CBoundsCheck,
    CIsStatic,
    CCallByValue,
    CVirtualName,
    CUnnamedObject,
    CTemporaryAvoided,
    CQualifier,
    CArrayIni,
    ROk,
    WOk,
    SuperClass,
    ExceptionsThrownList,
    CJavaMethodType,
    Compiled,
    PartialSpecializationArgs,
    SpecializationOf,
    InitArgs,
    Ambiguous,
    SpecializationTemplateArgs,
    FullTemplateArgs,
    InstantiatedWith,
    TemplateMethods,
    CppNotTypechecked,
    Noaccess,
    IsOperator,
    IsCastOperator,
    IsExplicit,
    IsMutable,
    VirtualName,
    IsPureVirtual,
    IsVtptr,
    Prefix,
    Cv,
    CppDummyDestructor,
    CastExpression,
    PodConstructor,
    TemplateDecls,
    ThrowDecl,
    Typeid,
    CQuoted,
    ToMember,
    PointerToMember,
    Tuple,
    FunctionBody,
    GetMay,
    SetMay,
    ClearMay,
    GetMust,
    SetMust,
    ClearMust,
    Pragma,
    StatementList,
    StatementListType,
    StatementListFunction,
    StatementListFunctionBlock,
    StatementListMainFunction,
    StatementListDataBlock,
    StatementListVersion,
    StatementListVarInput,
    StatementListVarInout,
    StatementListVarOutput,
    StatementListVarConstant,
    StatementListVarTemp,
    StatementListVarStatic,
    StatementListReturn,
    StatementListReturnValueId,
    StatementListVarEntry,
    StatementListVarDecls,
    StatementListNetwork,
    StatementListNetworks,
    StatementListTitle,
    StatementListIdentifier,
    StatementListLoad,
    StatementListTransfer,
    StatementListCall,
    StatementListNop,
    StatementListConstAdd,
    StatementListAccuIntAdd,
    StatementListAccuIntSub,
    StatementListAccuIntMul,
    StatementListAccuIntDiv,
    StatementListAccuIntEq,
    StatementListAccuIntNeq,
    StatementListAccuIntGt,
    StatementListAccuIntLt,
    StatementListAccuIntGte,
    StatementListAccuIntLte,
    StatementListAccuRealAdd,
    StatementListAccuRealSub,
    StatementListAccuRealMul,
    StatementListAccuRealDiv,
    StatementListAccuRealEq,
    StatementListAccuRealNeq,
    StatementListAccuRealGt,
    StatementListAccuRealLt,
    StatementListAccuRealGte,
    StatementListAccuRealLte,
    StatementListAccuDintAdd,
    StatementListAccuDintSub,
    StatementListAccuDintMul,
    StatementListAccuDintDiv,
    StatementListAccuDintEq,
    StatementListAccuDintNeq,
    StatementListAccuDintGt,
    StatementListAccuDintLt,
    StatementListAccuDintGte,
    StatementListAccuDintLte,
    StatementListAnd,
    StatementListAndNot,
    StatementListOr,
    StatementListOrNot,
    StatementListXor,
    StatementListXorNot,
    StatementListAndNested,
    StatementListAndNotNested,
    StatementListOrNested,
    StatementListOrNotNested,
    StatementListXorNested,
    StatementListXorNotNested,
    StatementListNestingClosed,
    StatementListAssign,
    StatementListSetRlo,
    StatementListClrRlo,
    StatementListSet,
    StatementListReset,
    StatementListNot,
    StatementListInstruction,
    StatementListInstructions,
    VectorEqual,
    VectorNotequal,
    VectorGe,
    VectorLe,
    VectorGt,
    VectorLt,
    FloatbvRoundToIntegral,
    ShuffleVector,
}

impl IrepId {
    pub fn from_int<T>(i: T) -> IrepId
    where
        T: Into<BigInt>,
    {
        IrepId::FreeformInteger(i.into())
    }

    /// CBMC expects two's complement for negative numbers.
    /// <https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424>
    /// The bignum crate instead does sign/magnitude when making hex.
    /// So for negatives, do the two's complement ourselves.
    pub fn bitpattern_from_int<T>(i: T, width: u64, _signed: bool) -> IrepId
    where
        T: Into<BigInt>,
    {
        let value: BigInt = i.into();
        // TODO https://github.com/model-checking/kani/issues/996
        // assert!(
        //     value.fits_in_bits(width, signed),
        //     "Cannot fit value into bits. value {} width: {} signed: {}",
        //     value,
        //     width,
        //     signed
        // );
        let bitpattern = if value.sign() == Sign::Minus {
            value.two_complement(width).to_biguint().unwrap()
        } else {
            value.to_biguint().unwrap()
        };
        IrepId::FreeformBitPattern(bitpattern)
    }

    //TODO assert that s is not the string produced by any other IrepId
    pub fn from_string<T: Into<InternedString>>(s: T) -> IrepId {
        IrepId::FreeformString(s.into())
    }
}

// Implementing `ToString` rather than `Display` because display only has the interface
// to write to a formatter which seems to be slower when you just need the string.
#[allow(clippy::to_string_trait_impl)]
impl ToString for IrepId {
    fn to_string(&self) -> String {
        self.to_string_cow().into_owned()
    }
}

impl IrepId {
    pub fn to_string_cow(&self) -> Cow<'_, str> {
        match self.to_owned_string() {
            Some(owned) => Cow::Owned(owned),
            None => Cow::Borrowed(self.to_static_string()),
        }
    }

    fn to_owned_string(&self) -> Option<String> {
        match self {
            IrepId::FreeformString(s) => Some(s.to_string()),
            IrepId::FreeformInteger(i) => Some(i.to_string()),
            IrepId::FreeformBitPattern(i) => Some(format!("{i:X}")),
            _ => None,
        }
    }

    fn to_static_string(&self) -> &'static str {
        match self {
            IrepId::FreeformString(_)
            | IrepId::FreeformInteger(_)
            | IrepId::FreeformBitPattern { .. } => unreachable!(),
            IrepId::EmptyString => "",
            IrepId::Let => "let",
            IrepId::LetBinding => "let_binding",
            IrepId::Nil => "nil",
            IrepId::Type => "type",
            IrepId::Bool => "bool",
            IrepId::CBool => "c_bool",
            IrepId::ProperBool => "proper_bool",
            IrepId::Signedbv => "signedbv",
            IrepId::Unsignedbv => "unsignedbv",
            IrepId::VerilogSignedbv => "verilog_signedbv",
            IrepId::VerilogUnsignedbv => "verilog_unsignedbv",
            IrepId::Floatbv => "floatbv",
            IrepId::Fixedbv => "fixedbv",
            IrepId::X86Extended => "x86_extended",
            IrepId::CSourceLocation => "#source_location",
            IrepId::CEndLocation => "#end_location",
            IrepId::CIsPadding => "#is_padding",
            IrepId::CDoNotDump => "C_do_not_dump",
            IrepId::File => "file",
            IrepId::Line => "line",
            IrepId::Column => "column",
            IrepId::Comment => "comment",
            IrepId::Property => "property",
            IrepId::PropertyClass => "property_class",
            IrepId::PropertyId => "property_id",
            IrepId::Function => "function",
            IrepId::MathematicalFunction => "mathematical_function",
            IrepId::Code => "code",
            IrepId::Typecast => "typecast",
            IrepId::StaticCast => "static_cast",
            IrepId::DynamicCast => "dynamic_cast",
            IrepId::ConstCast => "const_cast",
            IrepId::ReinterpretCast => "reinterpret_cast",
            IrepId::Index => "index",
            IrepId::Ptrmember => "ptrmember",
            IrepId::Member => "member",
            IrepId::MemberName => "member_name",
            IrepId::CMemberName => "#member_name",
            IrepId::Equal => "=",
            IrepId::Implies => "=>",
            IrepId::And => "and",
            IrepId::Nand => "nand",
            IrepId::Or => "or",
            IrepId::Nor => "nor",
            IrepId::Xor => "xor",
            IrepId::Not => "not",
            IrepId::Bitand => "bitand",
            IrepId::Bitor => "bitor",
            IrepId::Bitnot => "bitnot",
            IrepId::Bitxor => "bitxor",
            IrepId::Bitnand => "bitnand",
            IrepId::Bitnor => "bitnor",
            IrepId::Bitxnor => "bitxnor",
            IrepId::Notequal => "notequal",
            IrepId::If => "if",
            IrepId::Symbol => "symbol",
            IrepId::NextSymbol => "next_symbol",
            IrepId::NondetSymbol => "nondet_symbol",
            IrepId::PredicateSymbol => "predicate_symbol",
            IrepId::PredicateNextSymbol => "predicate_next_symbol",
            IrepId::NondetBool => "nondet_bool",
            IrepId::Empty => "empty",
            IrepId::SideEffect => "side_effect",
            IrepId::Statement => "statement",
            IrepId::StatementExpression => "statement_expression",
            IrepId::Value => "value",
            IrepId::Constant => "constant",
            IrepId::Block => "block",
            IrepId::Decl => "decl",
            IrepId::Dead => "dead",
            IrepId::Assign => "assign",
            IrepId::AssignDiv => "assign_div",
            IrepId::AssignMult => "assign*",
            IrepId::AssignPlus => "assign+",
            IrepId::AssignMinus => "assign-",
            IrepId::AssignMod => "assign_mod",
            IrepId::AssignShl => "assign_shl",
            IrepId::AssignShr => "assign_shr",
            IrepId::AssignAshr => "assign_ashr",
            IrepId::AssignLshr => "assign_lshr",
            IrepId::AssignBitand => "assign_bitand",
            IrepId::AssignBitxor => "assign_bitxor",
            IrepId::AssignBitor => "assign_bitor",
            IrepId::Assume => "assume",
            IrepId::Assert => "assert",
            IrepId::Assertion => "assertion",
            IrepId::Precondition => "precondition",
            IrepId::Postcondition => "postcondition",
            IrepId::PreconditionInstance => "precondition_instance",
            IrepId::Goto => "goto",
            IrepId::GccComputedGoto => "gcc_computed_goto",
            IrepId::Ifthenelse => "ifthenelse",
            IrepId::Label => "label",
            IrepId::Break => "break",
            IrepId::Continue => "continue",
            IrepId::FunctionCall => "function_call",
            IrepId::Return => "return",
            IrepId::Skip => "skip",
            IrepId::Arguments => "arguments",
            IrepId::Array => "array",
            IrepId::Size => "size",
            IrepId::FrontendPointer => "frontend_pointer",
            IrepId::Pointer => "pointer",
            IrepId::BlockPointer => "block_pointer",
            IrepId::Switch => "switch",
            IrepId::SwitchCase => "switch_case",
            IrepId::GccSwitchCaseRange => "gcc_switch_case_range",
            IrepId::For => "for",
            IrepId::While => "while",
            IrepId::Dowhile => "dowhile",
            IrepId::Int => "int",
            IrepId::Integer => "integer",
            IrepId::Natural => "natural",
            IrepId::Real => "real",
            IrepId::Rational => "rational",
            IrepId::Complex => "complex",
            IrepId::Signed => "signed",
            IrepId::Unsigned => "unsigned",
            IrepId::Asm => "asm",
            IrepId::GccAsmInput => "gcc_asm_input",
            IrepId::GccAsmOutput => "gcc_asm_output",
            IrepId::GccAsmClobberedRegister => "gcc_asm_clobbered_register",
            IrepId::Incomplete => "incomplete",
            IrepId::IncompleteClass => "incomplete_class",
            IrepId::CIncomplete => "#incomplete",
            IrepId::Identifier => "identifier",
            IrepId::Name => "name",
            IrepId::InnerName => "inner_name",
            IrepId::CppName => "cpp_name",
            IrepId::ComponentCppName => "component_cpp_name",
            IrepId::CIdClass => "#id_class",
            IrepId::Declaration => "declaration",
            IrepId::DeclarationList => "declaration_list",
            IrepId::Declarator => "declarator",
            IrepId::Struct => "struct",
            IrepId::CBitField => "c_bit_field",
            IrepId::Union => "union",
            IrepId::Class => "class",
            IrepId::MergedType => "merged_type",
            IrepId::Range => "range",
            IrepId::From => "from",
            IrepId::To => "to",
            IrepId::Module => "module",
            IrepId::Parameter => "parameter",
            IrepId::ComponentName => "component_name",
            IrepId::ComponentNumber => "component_number",
            IrepId::Tag => "tag",
            IrepId::Default => "default",
            IrepId::CDefaultValue => "#default_value",
            IrepId::BaseName => "base_name",
            IrepId::CBaseName => "#base_name",
            IrepId::String => "string",
            IrepId::CStringConstant => "#string_constant",
            IrepId::StringConstant => "string_constant",
            IrepId::Width => "width",
            IrepId::Components => "components",
            IrepId::Bv => "bv",
            IrepId::F => "f",
            IrepId::With => "with",
            IrepId::Trans => "trans",
            IrepId::Throw => "throw",
            IrepId::TryCatch => "try_catch",
            IrepId::Noexcept => "noexcept",
            IrepId::CPROVERThrow => "CPROVER_throw",
            IrepId::CPROVERTryCatch => "CPROVER_try_catch",
            IrepId::CPROVERTryFinally => "CPROVER_try_finally",
            IrepId::Protection => "protection",
            IrepId::Private => "private",
            IrepId::Public => "public",
            IrepId::Protected => "protected",
            IrepId::Virtual => "virtual",
            IrepId::Volatile => "volatile",
            IrepId::Const => "const",
            IrepId::Constexpr => "constexpr",
            IrepId::Inline => "inline",
            IrepId::Forall => "forall",
            IrepId::Exists => "exists",
            IrepId::Repeat => "repeat",
            IrepId::Extractbit => "extractbit",
            IrepId::Extractbits => "extractbits",
            IrepId::CReference => "#reference",
            IrepId::CRvalueReference => "#rvalue_reference",
            IrepId::True => "true",
            IrepId::False => "false",
            IrepId::AddressOf => "address_of",
            IrepId::Dereference => "dereference",
            IrepId::CLvalue => "#lvalue",
            IrepId::CBase => "#base",
            IrepId::Destination => "destination",
            IrepId::Main => "main",
            IrepId::Expression => "expression",
            IrepId::Allocate => "allocate",
            IrepId::CCxxAllocType => "#cxx_alloc_type",
            IrepId::CppNew => "cpp_new",
            IrepId::CppDelete => "cpp_delete",
            IrepId::CppNewArray => "cpp_new[]",
            IrepId::CppDeleteArray => "cpp_delete[]",
            IrepId::JavaNew => "java_new",
            IrepId::JavaNewArray => "java_new_array",
            IrepId::JavaNewArrayData => "java_new_array_data",
            IrepId::JavaStringLiteral => "java_string_literal",
            IrepId::Printf => "printf",
            IrepId::Input => "input",
            IrepId::Output => "output",
            IrepId::Nondet => "nondet",
            IrepId::NULL => "NULL",
            IrepId::Null => "null",
            IrepId::Nullptr => "nullptr",
            IrepId::CEnum => "c_enum",
            IrepId::Enumeration => "enumeration",
            IrepId::Elements => "elements",
            IrepId::Unknown => "unknown",
            IrepId::Uninitialized => "uninitialized",
            IrepId::Invalid => "invalid",
            IrepId::CInvalidObject => "#invalid_object",
            IrepId::PointerOffset => "pointer_offset",
            IrepId::PointerObject => "pointer_object",
            IrepId::IsInvalidPointer => "is_invalid_pointer",
            IrepId::IeeeFloatEqual => "ieee_float_equal",
            IrepId::IeeeFloatNotequal => "ieee_float_notequal",
            IrepId::Isnan => "isnan",
            IrepId::Lambda => "lambda",
            IrepId::ArrayComprehension => "array_comprehension",
            IrepId::ArrayOf => "array_of",
            IrepId::ArrayEqual => "array_equal",
            IrepId::ArraySet => "array_set",
            IrepId::ArrayCopy => "array_copy",
            IrepId::ArrayList => "array_list",
            IrepId::Mod => "mod",
            IrepId::Rem => "rem",
            IrepId::Shr => "shr",
            IrepId::Ashr => "ashr",
            IrepId::Lshr => "lshr",
            IrepId::Shl => "shl",
            IrepId::Rol => "rol",
            IrepId::Ror => "ror",
            IrepId::Comma => "comma",
            IrepId::Concatenation => "concatenation",
            IrepId::Infinity => "infinity",
            IrepId::ReturnType => "return_type",
            IrepId::Typedef => "typedef",
            IrepId::TypedefType => "typedef_type",
            IrepId::CTypedef => "#typedef",
            IrepId::Extern => "extern",
            IrepId::Static => "static",
            IrepId::Auto => "auto",
            IrepId::Register => "register",
            IrepId::ThreadLocal => "thread_local",
            IrepId::Thread => "thread",
            IrepId::CThreadLocal => "#thread_local",
            IrepId::CStaticLifetime => "#static_lifetime",
            IrepId::Mutable => "mutable",
            IrepId::Void => "void",
            IrepId::Int8 => "int8",
            IrepId::Int16 => "int16",
            IrepId::Int32 => "int32",
            IrepId::Int64 => "int64",
            IrepId::Ptr32 => "ptr32",
            IrepId::Ptr64 => "ptr64",
            IrepId::Char => "char",
            IrepId::Short => "short",
            IrepId::Long => "long",
            IrepId::Float => "float",
            IrepId::Float16 => "float16",
            IrepId::Float128 => "float128",
            IrepId::Double => "double",
            IrepId::Byte => "byte",
            IrepId::Boolean => "boolean",
            IrepId::LongDouble => "long_double",
            IrepId::SignedChar => "signed_char",
            IrepId::UnsignedChar => "unsigned_char",
            IrepId::SignedInt => "signed_int",
            IrepId::UnsignedInt => "unsigned_int",
            IrepId::SignedLongInt => "signed_long_int",
            IrepId::UnsignedLongInt => "unsigned_long_int",
            IrepId::SignedShortInt => "signed_short_int",
            IrepId::UnsignedShortInt => "unsigned_short_int",
            IrepId::SignedLongLongInt => "signed_long_long_int",
            IrepId::UnsignedLongLongInt => "unsigned_long_long_int",
            IrepId::SignedInt128 => "signed_int128",
            IrepId::UnsignedInt128 => "unsigned_int128",
            IrepId::Case => "case",
            IrepId::CInlined => "#inlined",
            IrepId::CHide => "#hide",
            IrepId::Hide => "hide",
            IrepId::Abs => "abs",
            IrepId::Sign => "sign",
            IrepId::Access => "access",
            IrepId::CAccess => "#access",
            IrepId::Postincrement => "postincrement",
            IrepId::Postdecrement => "postdecrement",
            IrepId::Preincrement => "preincrement",
            IrepId::Predecrement => "predecrement",
            IrepId::IntegerBits => "integer_bits",
            IrepId::KnR => "KnR",
            IrepId::CKnR => "#KnR",
            IrepId::ConstraintSelectOne => "constraint_select_one",
            IrepId::Cond => "cond",
            IrepId::BvLiterals => "bv_literals",
            IrepId::IsFinite => "isfinite",
            IrepId::Isinf => "isinf",
            IrepId::Isnormal => "isnormal",
            IrepId::Alignof => "alignof",
            IrepId::ClangBuiltinConvertvector => "clang_builtin_convertvector",
            IrepId::GccBuiltinVaArg => "gcc_builtin_va_arg",
            IrepId::GccBuiltinTypesCompatibleP => "gcc_builtin_types_compatible_p",
            IrepId::VaStart => "va_start",
            IrepId::GccFloat16 => "gcc_float16",
            IrepId::GccFloat32 => "gcc_float32",
            IrepId::GccFloat32x => "gcc_float32x",
            IrepId::GccFloat64 => "gcc_float64",
            IrepId::GccFloat64x => "gcc_float64x",
            IrepId::GccFloat80 => "gcc_float80",
            IrepId::GccFloat128 => "gcc_float128",
            IrepId::GccFloat128x => "gcc_float128x",
            IrepId::GccInt128 => "gcc_int128",
            IrepId::GccDecimal32 => "gcc_decimal32",
            IrepId::GccDecimal64 => "gcc_decimal64",
            IrepId::GccDecimal128 => "gcc_decimal128",
            IrepId::BuiltinOffsetof => "builtin_offsetof",
            IrepId::Id0 => "0",
            IrepId::Id1 => "1",
            IrepId::Sizeof => "sizeof",
            IrepId::TypeArg => "type_arg",
            IrepId::ExprArg => "expr_arg",
            IrepId::ExpressionList => "expression_list",
            IrepId::InitializerList => "initializer_list",
            IrepId::GccConditionalExpression => "gcc_conditional_expression",
            IrepId::GccLocalLabel => "gcc_local_label",
            IrepId::Gcc => "gcc",
            IrepId::Msc => "msc",
            IrepId::Typeof => "typeof",
            IrepId::Ellipsis => "ellipsis",
            IrepId::Flavor => "flavor",
            IrepId::Ge => ">=",
            IrepId::Le => "<=",
            IrepId::Gt => ">",
            IrepId::Lt => "<",
            IrepId::Plus => "+",
            IrepId::Minus => "-",
            IrepId::UnaryMinus => "unary-",
            IrepId::UnaryPlus => "unary+",
            IrepId::Mult => "*",
            IrepId::Div => "/",
            IrepId::Power => "**",
            IrepId::FactorialPower => "factorial_power",
            IrepId::CPrettyName => "#pretty_name",
            IrepId::CClass => "#class",
            IrepId::CField => "#field",
            IrepId::CInterface => "#interface",
            IrepId::DesignatedInitializer => "designated_initializer",
            IrepId::Designator => "designator",
            IrepId::MemberDesignator => "member_designator",
            IrepId::IndexDesignator => "index_designator",
            IrepId::CConstant => "#constant",
            IrepId::CVolatile => "#volatile",
            IrepId::CRestricted => "#restricted",
            IrepId::CIdentifier => "#identifier",
            IrepId::CImplicit => "#implicit",
            IrepId::CPtr32 => "#ptr32",
            IrepId::CPtr64 => "#ptr64",
            IrepId::CAtomic => "#atomic",
            IrepId::Restrict => "restrict",
            IrepId::ByteExtractBigEndian => "byte_extract_big_endian",
            IrepId::ByteExtractLittleEndian => "byte_extract_little_endian",
            IrepId::ByteUpdateBigEndian => "byte_update_big_endian",
            IrepId::ByteUpdateLittleEndian => "byte_update_little_endian",
            IrepId::Replication => "replication",
            IrepId::CproverAtomic => "cprover_atomic",
            IrepId::Atomic => "atomic",
            IrepId::AtomicTypeSpecifier => "atomic_type_specifier",
            IrepId::AtomicBegin => "atomic_begin",
            IrepId::AtomicEnd => "atomic_end",
            IrepId::StartThread => "start_thread",
            IrepId::EndThread => "end_thread",
            IrepId::CoverageCriterion => "coverage_criterion",
            IrepId::Initializer => "initializer",
            IrepId::Anonymous => "anonymous",
            IrepId::CIsAnonymous => "#is_anonymous",
            IrepId::IsEnumConstant => "is_enum_constant",
            IrepId::IsInline => "is_inline",
            IrepId::IsExtern => "is_extern",
            IrepId::IsSynchronized => "is_synchronized",
            IrepId::IsNativeMethod => "is_native_method",
            IrepId::IsVarargsMethod => "is_varargs_method",
            IrepId::IsGlobal => "is_global",
            IrepId::IsThreadLocal => "is_thread_local",
            IrepId::IsParameter => "is_parameter",
            IrepId::IsMember => "is_member",
            IrepId::IsType => "is_type",
            IrepId::IsRegister => "is_register",
            IrepId::IsTypedef => "is_typedef",
            IrepId::IsStatic => "is_static",
            IrepId::IsTemplate => "is_template",
            IrepId::IsStaticAssert => "is_static_assert",
            IrepId::IsVirtual => "is_virtual",
            IrepId::CIsVirtual => "#is_virtual",
            IrepId::Literal => "literal",
            IrepId::MemberInitializers => "member_initializers",
            IrepId::MemberInitializer => "member_initializer",
            IrepId::MethodQualifier => "method_qualifier",
            IrepId::Methods => "methods",
            IrepId::StaticMembers => "static_members",
            IrepId::Constructor => "constructor",
            IrepId::Destructor => "destructor",
            IrepId::Bases => "bases",
            IrepId::Base => "base",
            IrepId::FromBase => "from_base",
            IrepId::Operator => "operator",
            IrepId::Template => "template",
            IrepId::TemplateClassInstance => "template_class_instance",
            IrepId::TemplateFunctionInstance => "template_function_instance",
            IrepId::TemplateType => "template_type",
            IrepId::TemplateArgs => "template_args",
            IrepId::TemplateParameter => "template_parameter",
            IrepId::TemplateParameterSymbolType => "template_parameter_symbol_type",
            IrepId::TemplateParameters => "template_parameters",
            IrepId::CTemplate => "#template",
            IrepId::CTemplateArguments => "#template_arguments",
            IrepId::CTemplateCase => "#template_case",
            IrepId::Typename => "typename",
            IrepId::C => "C",
            IrepId::Cpp => "cpp",
            IrepId::Java => "java",
            IrepId::DeclBlock => "decl_block",
            IrepId::DeclType => "decl_type",
            IrepId::Parameters => "parameters",
            IrepId::WcharT => "wchar_t",
            IrepId::Char16T => "char16_t",
            IrepId::Char32T => "char32_t",
            IrepId::SizeT => "size_t",
            IrepId::SsizeT => "ssize_t",
            IrepId::Mode => "mode",
            IrepId::This => "this",
            IrepId::CThis => "#this",
            IrepId::ReductionAnd => "reduction_and",
            IrepId::ReductionOr => "reduction_or",
            IrepId::ReductionNand => "reduction_nand",
            IrepId::ReductionNor => "reduction_nor",
            IrepId::ReductionXor => "reduction_xor",
            IrepId::ReductionXnor => "reduction_xnor",
            IrepId::CZeroInitializer => "#zero_initializer",
            IrepId::Body => "body",
            IrepId::TemporaryObject => "temporary_object",
            IrepId::OverflowPlus => "overflow-+",
            IrepId::OverflowMinus => "overflow--",
            IrepId::OverflowMult => "overflow-*",
            IrepId::OverflowResultPlus => "overflow_result-+",
            IrepId::OverflowResultMinus => "overflow_result--",
            IrepId::OverflowResultMult => "overflow_result-*",
            IrepId::OverflowUnaryMinus => "overflow-unary-",
            IrepId::ObjectDescriptor => "object_descriptor",
            IrepId::IsDynamicObject => "is_dynamic_object",
            IrepId::DynamicObject => "dynamic_object",
            IrepId::CDynamic => "#dynamic",
            IrepId::ObjectSize => "object_size",
            IrepId::GoodPointer => "good_pointer",
            IrepId::IntegerAddress => "integer_address",
            IrepId::IntegerAddressObject => "integer_address_object",
            IrepId::NullObject => "NULL-object",
            IrepId::StaticObject => "static_object",
            IrepId::StackObject => "stack_object",
            IrepId::CIsFailedSymbol => "#is_failed_symbol",
            IrepId::CFailedSymbol => "#failed_symbol",
            IrepId::Friend => "friend",
            IrepId::CFriends => "#friends",
            IrepId::Explicit => "explicit",
            IrepId::StorageSpec => "storage_spec",
            IrepId::MemberSpec => "member_spec",
            IrepId::MscDeclspec => "msc_declspec",
            IrepId::Packed => "packed",
            IrepId::CPacked => "#packed",
            IrepId::TransparentUnion => "transparent_union",
            IrepId::CTransparentUnion => "#transparent_union",
            IrepId::Aligned => "aligned",
            IrepId::CAlignment => "#alignment",
            IrepId::FrontendVector => "frontend_vector",
            IrepId::Vector => "vector",
            IrepId::Abstract => "abstract",
            IrepId::FunctionApplication => "function_application",
            IrepId::CppDeclarator => "cpp_declarator",
            IrepId::CppLinkageSpec => "cpp_linkage_spec",
            IrepId::CppNamespaceSpec => "cpp_namespace_spec",
            IrepId::CppStorageSpec => "cpp_storage_spec",
            IrepId::CppUsing => "cpp_using",
            IrepId::CppDeclaration => "cpp_declaration",
            IrepId::CppStaticAssert => "cpp_static_assert",
            IrepId::CppMemberSpec => "cpp_member_spec",
            IrepId::CCType => "#c_type",
            IrepId::Namespace => "namespace",
            IrepId::Linkage => "linkage",
            IrepId::Decltype => "decltype",
            IrepId::CTagOnlyDeclaration => "#tag_only_declaration",
            IrepId::StructTag => "struct_tag",
            IrepId::UnionTag => "union_tag",
            IrepId::CEnumTag => "c_enum_tag",
            IrepId::VerilogCaseEquality => "verilog_case_equality",
            IrepId::VerilogCaseInequality => "verilog_case_inequality",
            IrepId::UserSpecifiedPredicate => "user_specified_predicate",
            IrepId::UserSpecifiedParameterPredicates => "user_specified_parameter_predicates",
            IrepId::UserSpecifiedReturnPredicates => "user_specified_return_predicates",
            IrepId::Unassigned => "unassigned",
            IrepId::NewObject => "new_object",
            IrepId::ComplexReal => "complex_real",
            IrepId::ComplexImag => "complex_imag",
            IrepId::Imag => "imag",
            IrepId::MscTryExcept => "msc_try_except",
            IrepId::MscTryFinally => "msc_try_finally",
            IrepId::MscLeave => "msc_leave",
            IrepId::MscUuidof => "msc_uuidof",
            IrepId::MscIfExists => "msc_if_exists",
            IrepId::MscIfNotExists => "msc_if_not_exists",
            IrepId::MscUnderlyingType => "msc_underlying_type",
            IrepId::MscBased => "msc_based",
            IrepId::Alias => "alias",
            IrepId::PtrObject => "ptr_object",
            IrepId::CCSizeofType => "#c_sizeof_type",
            IrepId::ArrayUpdate => "array_update",
            IrepId::Update => "update",
            IrepId::StaticAssert => "static_assert",
            IrepId::GccAttributeMode => "gcc_attribute_mode",
            IrepId::BuiltIn => "<built-in>",
            IrepId::ExceptionList => "exception_list",
            IrepId::ExceptionId => "exception_id",
            IrepId::PredicatePassiveSymbol => "predicate_passive_symbol",
            IrepId::CwVaArgTypeof => "cw_va_arg_typeof",
            IrepId::Fence => "fence",
            IrepId::Sync => "sync",
            IrepId::Lwsync => "lwsync",
            IrepId::Isync => "isync",
            IrepId::WRfence => "WRfence",
            IrepId::RRfence => "RRfence",
            IrepId::RWfence => "RWfence",
            IrepId::WWfence => "WWfence",
            IrepId::RRcumul => "RRcumul",
            IrepId::RWcumul => "RWcumul",
            IrepId::WWcumul => "WWcumul",
            IrepId::WRcumul => "WRcumul",
            IrepId::GenericSelection => "generic_selection",
            IrepId::GenericAssociations => "generic_associations",
            IrepId::GenericAssociation => "generic_association",
            IrepId::FloatbvPlus => "floatbv_plus",
            IrepId::FloatbvMinus => "floatbv_minus",
            IrepId::FloatbvMult => "floatbv_mult",
            IrepId::FloatbvDiv => "floatbv_div",
            IrepId::FloatbvRem => "floatbv_rem",
            IrepId::FloatbvTypecast => "floatbv_typecast",
            IrepId::CompoundLiteral => "compound_literal",
            IrepId::CustomBv => "custom_bv",
            IrepId::CustomUnsignedbv => "custom_unsignedbv",
            IrepId::CustomSignedbv => "custom_signedbv",
            IrepId::CustomFixedbv => "custom_fixedbv",
            IrepId::CustomFloatbv => "custom_floatbv",
            IrepId::CSSASymbol => "#SSA_symbol",
            IrepId::L0 => "L0",
            IrepId::L1 => "L1",
            IrepId::L2 => "L2",
            IrepId::L1ObjectIdentifier => "L1_object_identifier",
            IrepId::AlreadyTypechecked => "already_typechecked",
            IrepId::CVaArgType => "#va_arg_type",
            IrepId::Smt2Symbol => "smt2_symbol",
            IrepId::Onehot => "onehot",
            IrepId::Onehot0 => "onehot0",
            IrepId::Popcount => "popcount",
            IrepId::CountLeadingZeros => "count_leading_zeros",
            IrepId::CountTrailingZeros => "count_trailing_zeros",
            IrepId::EmptyUnion => "empty_union",
            IrepId::FunctionType => "function_type",
            IrepId::Noreturn => "noreturn",
            IrepId::CNoreturn => "#noreturn",
            IrepId::Weak => "weak",
            IrepId::IsWeak => "is_weak",
            IrepId::Used => "used",
            IrepId::IsUsed => "is_used",
            IrepId::CSpecLoopInvariant => "#spec_loop_invariant",
            IrepId::CSpecRequires => "#spec_requires",
            IrepId::CSpecEnsures => "#spec_ensures",
            IrepId::CSpecAssigns => "#spec_assigns",
            IrepId::VirtualFunction => "virtual_function",
            IrepId::ElementType => "element_type",
            IrepId::WorkingDirectory => "working_directory",
            IrepId::Section => "section",
            IrepId::Bswap => "bswap",
            IrepId::BitReverse => "bitreverse",
            IrepId::JavaBytecodeIndex => "java_bytecode_index",
            IrepId::JavaInstanceof => "java_instanceof",
            IrepId::JavaSuperMethodCall => "java_super_method_call",
            IrepId::JavaEnumStaticUnwind => "java_enum_static_unwind",
            IrepId::PushCatch => "push_catch",
            IrepId::PopCatch => "pop_catch",
            IrepId::ExceptionLandingpad => "exception_landingpad",
            IrepId::LengthUpperBound => "length_upper_bound",
            IrepId::CproverAssociateArrayToPointerFunc => "cprover_associate_array_to_pointer_func",
            IrepId::CproverAssociateLengthToArrayFunc => "cprover_associate_length_to_array_func",
            IrepId::CproverCharLiteralFunc => "cprover_char_literal_func",
            IrepId::CproverStringLiteralFunc => "cprover_string_literal_func",
            IrepId::CproverStringCharAtFunc => "cprover_string_char_at_func",
            IrepId::CproverStringCharSetFunc => "cprover_string_char_set_func",
            IrepId::CproverStringCodePointAtFunc => "cprover_string_code_point_at_func",
            IrepId::CproverStringCodePointBeforeFunc => "cprover_string_code_point_before_func",
            IrepId::CproverStringCodePointCountFunc => "cprover_string_code_point_count_func",
            IrepId::CproverStringOffsetByCodePointFunc => {
                "cprover_string_offset_by_code_point_func"
            }
            IrepId::CproverStringCompareToFunc => "cprover_string_compare_to_func",
            IrepId::CproverStringConcatFunc => "cprover_string_concat_func",
            IrepId::CproverStringConcatCharFunc => "cprover_string_concat_char_func",
            IrepId::CproverStringConcatCodePointFunc => "cprover_string_concat_code_point_func",
            IrepId::CproverStringConstrainCharactersFunc => {
                "cprover_string_constrain_characters_func"
            }
            IrepId::CproverStringContainsFunc => "cprover_string_contains_func",
            IrepId::CproverStringCopyFunc => "cprover_string_copy_func",
            IrepId::CproverStringDeleteFunc => "cprover_string_delete_func",
            IrepId::CproverStringDeleteCharAtFunc => "cprover_string_delete_char_at_func",
            IrepId::CproverStringEqualFunc => "cprover_string_equal_func",
            IrepId::CproverStringEqualsIgnoreCaseFunc => "cprover_string_equals_ignore_case_func",
            IrepId::CproverStringEmptyStringFunc => "cprover_string_empty_string_func",
            IrepId::CproverStringEndswithFunc => "cprover_string_endswith_func",
            IrepId::CproverStringFormatFunc => "cprover_string_format_func",
            IrepId::CproverStringIndexOfFunc => "cprover_string_index_of_func",
            IrepId::CproverStringInsertFunc => "cprover_string_insert_func",
            IrepId::CproverStringIsPrefixFunc => "cprover_string_is_prefix_func",
            IrepId::CproverStringIsSuffixFunc => "cprover_string_is_suffix_func",
            IrepId::CproverStringIsEmptyFunc => "cprover_string_is_empty_func",
            IrepId::CproverStringLastIndexOfFunc => "cprover_string_last_index_of_func",
            IrepId::CproverStringLengthFunc => "cprover_string_length_func",
            IrepId::CproverStringOfIntFunc => "cprover_string_of_int_func",
            IrepId::CproverStringOfIntHexFunc => "cprover_string_of_int_hex_func",
            IrepId::CproverStringOfLongFunc => "cprover_string_of_long_func",
            IrepId::CproverStringOfFloatFunc => "cprover_string_of_float_func",
            IrepId::CproverStringOfFloatScientificNotationFunc => {
                "cprover_string_of_float_scientific_notation_func"
            }
            IrepId::CproverStringOfDoubleFunc => "cprover_string_of_double_func",
            IrepId::CproverStringParseIntFunc => "cprover_string_parse_int_func",
            IrepId::CproverStringIsValidIntFunc => "cprover_string_is_valid_int_func",
            IrepId::CproverStringIsValidLongFunc => "cprover_string_is_valid_long_func",
            IrepId::CproverStringReplaceFunc => "cprover_string_replace_func",
            IrepId::CproverStringSetLengthFunc => "cprover_string_set_length_func",
            IrepId::CproverStringStartswithFunc => "cprover_string_startswith_func",
            IrepId::CproverStringSubstringFunc => "cprover_string_substring_func",
            IrepId::CproverStringToLowerCaseFunc => "cprover_string_to_lower_case_func",
            IrepId::CproverStringToUpperCaseFunc => "cprover_string_to_upper_case_func",
            IrepId::CproverStringTrimFunc => "cprover_string_trim_func",
            IrepId::SkipInitialize => "skip_initialize",
            IrepId::BasicBlockCoveredLines => "basic_block_covered_lines",
            IrepId::BasicBlockSourceLines => "basic_block_source_lines",
            IrepId::IsNondetNullable => "is_nondet_nullable",
            IrepId::ArrayReplace => "array_replace",
            IrepId::SwitchCaseNumber => "switch_case_number",
            IrepId::JavaArrayAccess => "java_array_access",
            IrepId::JavaMemberAccess => "java_member_access",
            IrepId::CJavaGenericParameter => "#java_generic_parameter",
            IrepId::CJavaGenericsClassType => "#java_generics_class_type",
            IrepId::CJavaImplicitlyGenericClassType => "#java_implicitly_generic_class_type",
            IrepId::CJavaGenericSymbol => "#java_generic_symbol",
            IrepId::GenericTypes => "generic_types",
            IrepId::ImplicitGenericTypes => "#implicit_generic_types",
            IrepId::TypeVariables => "type_variables",
            IrepId::HandleType => "handle_type",
            IrepId::JavaLambdaMethodHandle => "java_lambda_method_handle",
            IrepId::JavaLambdaMethodHandleIndex => "lambda_method_handle_index",
            IrepId::JavaLambdaMethodHandles => "lambda_method_handles",
            IrepId::HavocObject => "havoc_object",
            IrepId::OverflowShl => "overflow-shl",
            IrepId::CNoInitializationRequired => "#no_initialization_required",
            IrepId::CNoNondetInitialization => "#no_nondet_initialization",
            IrepId::OverlayClass => "java::org.cprover.OverlayClassImplementation",
            IrepId::OverlayMethod => "java::org.cprover.OverlayMethodImplementation",
            IrepId::IgnoredMethod => "java::org.cprover.IgnoredMethodImplementation",
            IrepId::IsAnnotation => "is_annotation",
            IrepId::CAnnotations => "#annotations",
            IrepId::Final => "final",
            IrepId::BitsPerByte => "bits_per_byte",
            IrepId::CAbstract => "#abstract",
            IrepId::Synthetic => "synthetic",
            IrepId::Interface => "interface",
            IrepId::CMustNotThrow => "#must_not_throw",
            IrepId::IsInnerClass => "is_inner_class",
            IrepId::IsAnonymous => "is_anonymous",
            IrepId::OuterClass => "outer_class",
            IrepId::IsBridgeMethod => "is_bridge_method",
            IrepId::CIsOperator => "#is_operator",
            IrepId::CNotAccessible => "#not_accessible",
            IrepId::COverrideConstantness => "#override_constantness",
            IrepId::CBound => "#bound",
            IrepId::CBoundsCheck => "#bounds_check",
            IrepId::CIsStatic => "#is_static",
            IrepId::CCallByValue => "#call_by_value",
            IrepId::CVirtualName => "#virtual_name",
            IrepId::CUnnamedObject => "#unnamed_object",
            IrepId::CTemporaryAvoided => "#temporary_avoided",
            IrepId::CQualifier => "#qualifier",
            IrepId::CArrayIni => "#array_ini",
            IrepId::ROk => "r_ok",
            IrepId::WOk => "w_ok",
            IrepId::SuperClass => "super_class",
            IrepId::ExceptionsThrownList => "exceptions_thrown_list",
            IrepId::CJavaMethodType => "#java_method_type",
            IrepId::Compiled => "compiled",
            IrepId::PartialSpecializationArgs => "partial_specialization_args",
            IrepId::SpecializationOf => "specialization_of",
            IrepId::InitArgs => "init_args",
            IrepId::Ambiguous => "ambiguous",
            IrepId::SpecializationTemplateArgs => "specialization_template_args",
            IrepId::FullTemplateArgs => "full_template_args",
            IrepId::InstantiatedWith => "instantiated_with",
            IrepId::TemplateMethods => "template_methods",
            IrepId::CppNotTypechecked => "cpp_not_typechecked",
            IrepId::Noaccess => "noaccess",
            IrepId::IsOperator => "is_operator",
            IrepId::IsCastOperator => "is_cast_operator",
            IrepId::IsExplicit => "is_explicit",
            IrepId::IsMutable => "is_mutable",
            IrepId::VirtualName => "virtual_name",
            IrepId::IsPureVirtual => "is_pure_virtual",
            IrepId::IsVtptr => "is_vtptr",
            IrepId::Prefix => "prefix",
            IrepId::Cv => "cv",
            IrepId::CppDummyDestructor => "cpp_dummy_destructor",
            IrepId::CastExpression => "cast_expression",
            IrepId::PodConstructor => "pod_constructor",
            IrepId::TemplateDecls => "template_decls",
            IrepId::ThrowDecl => "throw_decl",
            IrepId::Typeid => "typeid",
            IrepId::CQuoted => "#quoted",
            IrepId::ToMember => "to_member",
            IrepId::PointerToMember => "pointer_to_member",
            IrepId::Tuple => "tuple",
            IrepId::FunctionBody => "function_body",
            IrepId::GetMay => "get_may",
            IrepId::SetMay => "set_may",
            IrepId::ClearMay => "clear_may",
            IrepId::GetMust => "get_must",
            IrepId::SetMust => "set_must",
            IrepId::ClearMust => "clear_must",
            IrepId::Pragma => "pragma",
            IrepId::StatementList => "Statement List",
            IrepId::StatementListType => "statement_list_type",
            IrepId::StatementListFunction => "statement_list_function",
            IrepId::StatementListFunctionBlock => "statement_list_function_block",
            IrepId::StatementListMainFunction => "Main",
            IrepId::StatementListDataBlock => "statement_list_data_block",
            IrepId::StatementListVersion => "statement_list_version",
            IrepId::StatementListVarInput => "statement_list_var_input",
            IrepId::StatementListVarInout => "statement_list_var_inout",
            IrepId::StatementListVarOutput => "statement_list_var_output",
            IrepId::StatementListVarConstant => "statement_list_var_constant",
            IrepId::StatementListVarTemp => "statement_list_var_temp",
            IrepId::StatementListVarStatic => "statement_list_var_static",
            IrepId::StatementListReturn => "statement_list_return",
            IrepId::StatementListReturnValueId => "Ret_Val",
            IrepId::StatementListVarEntry => "statement_list_var_entry",
            IrepId::StatementListVarDecls => "statement_list_var_decls",
            IrepId::StatementListNetwork => "statement_list_network",
            IrepId::StatementListNetworks => "statement_list_networks",
            IrepId::StatementListTitle => "statement_list_title",
            IrepId::StatementListIdentifier => "statement_list_identifier",
            IrepId::StatementListLoad => "statement_list_load",
            IrepId::StatementListTransfer => "statement_list_transfer",
            IrepId::StatementListCall => "statement_list_call",
            IrepId::StatementListNop => "statement_list_nop",
            IrepId::StatementListConstAdd => "statement_list_const_add",
            IrepId::StatementListAccuIntAdd => "statement_list_accu_int_add",
            IrepId::StatementListAccuIntSub => "statement_list_accu_int_sub",
            IrepId::StatementListAccuIntMul => "statement_list_accu_int_mul",
            IrepId::StatementListAccuIntDiv => "statement_list_accu_int_div",
            IrepId::StatementListAccuIntEq => "statement_list_accu_int_eq",
            IrepId::StatementListAccuIntNeq => "statement_list_accu_int_neq",
            IrepId::StatementListAccuIntGt => "statement_list_accu_int_gt",
            IrepId::StatementListAccuIntLt => "statement_list_accu_int_lt",
            IrepId::StatementListAccuIntGte => "statement_list_accu_int_gte",
            IrepId::StatementListAccuIntLte => "statement_list_accu_int_lte",
            IrepId::StatementListAccuRealAdd => "statement_list_accu_real_add",
            IrepId::StatementListAccuRealSub => "statement_list_accu_real_sub",
            IrepId::StatementListAccuRealMul => "statement_list_accu_real_mul",
            IrepId::StatementListAccuRealDiv => "statement_list_accu_real_div",
            IrepId::StatementListAccuRealEq => "statement_list_accu_real_eq",
            IrepId::StatementListAccuRealNeq => "statement_list_accu_real_neq",
            IrepId::StatementListAccuRealGt => "statement_list_accu_real_gt",
            IrepId::StatementListAccuRealLt => "statement_list_accu_real_lt",
            IrepId::StatementListAccuRealGte => "statement_list_accu_real_gte",
            IrepId::StatementListAccuRealLte => "statement_list_accu_real_lte",
            IrepId::StatementListAccuDintAdd => "statement_list_accu_dint_add",
            IrepId::StatementListAccuDintSub => "statement_list_accu_dint_sub",
            IrepId::StatementListAccuDintMul => "statement_list_accu_dint_mul",
            IrepId::StatementListAccuDintDiv => "statement_list_accu_dint_div",
            IrepId::StatementListAccuDintEq => "statement_list_accu_dint_eq",
            IrepId::StatementListAccuDintNeq => "statement_list_accu_dint_neq",
            IrepId::StatementListAccuDintGt => "statement_list_accu_dint_gt",
            IrepId::StatementListAccuDintLt => "statement_list_accu_dint_lt",
            IrepId::StatementListAccuDintGte => "statement_list_accu_dint_gte",
            IrepId::StatementListAccuDintLte => "statement_list_accu_dint_lte",
            IrepId::StatementListAnd => "statement_list_and",
            IrepId::StatementListAndNot => "statement_list_and_not",
            IrepId::StatementListOr => "statement_list_or",
            IrepId::StatementListOrNot => "statement_list_or_not",
            IrepId::StatementListXor => "statement_list_xor",
            IrepId::StatementListXorNot => "statement_list_xor_not",
            IrepId::StatementListAndNested => "statement_list_and_nested",
            IrepId::StatementListAndNotNested => "statement_list_and_not_nested",
            IrepId::StatementListOrNested => "statement_list_or_nested",
            IrepId::StatementListOrNotNested => "statement_list_or_not_nested",
            IrepId::StatementListXorNested => "statement_list_xor_nested",
            IrepId::StatementListXorNotNested => "statement_list_xor_not_nested",
            IrepId::StatementListNestingClosed => "statement_list_nesting_closed",
            IrepId::StatementListAssign => "statement_list_assign",
            IrepId::StatementListSetRlo => "statement_list_set_rlo",
            IrepId::StatementListClrRlo => "statement_list_clr_rlo",
            IrepId::StatementListSet => "statement_list_set",
            IrepId::StatementListReset => "statement_list_reset",
            IrepId::StatementListNot => "statement_list_not",
            IrepId::StatementListInstruction => "statement_list_instruction",
            IrepId::StatementListInstructions => "statement_list_instructions",
            IrepId::VectorEqual => "vector-=",
            IrepId::VectorNotequal => "vector-!=",
            IrepId::VectorGe => "vector->=",
            IrepId::VectorLe => "vector-<=",
            IrepId::VectorGt => "vector->",
            IrepId::VectorLt => "vector-<",
            IrepId::FloatbvRoundToIntegral => "floatbv_round_to_integral",
            IrepId::ShuffleVector => "shuffle_vector",
        }
    }
}

#[cfg(test)]
mod tests {
    use crate::irep::IrepId;
    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic1() {
    //     IrepId::hex_from_int(-127, 7, true);
    // }

    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic2() {
    //     IrepId::hex_from_int(12, 4, true);
    // }

    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic3() {
    //     IrepId::hex_from_int(-12, 4, true);
    // }

    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic_string1() {
    //     IrepId::FreeformHexInteger { value: BigInt::from(-127), width: 7, signed: true }
    //         .to_string();
    // }

    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic_string2() {
    //     IrepId::FreeformHexInteger { value: BigInt::from(12), width: 4, signed: true }.to_string();
    // }

    // #[test]
    // #[should_panic]
    // fn test_hex_id_panic_string3() {
    //     IrepId::FreeformHexInteger { value: BigInt::from(-12), width: 4, signed: true }.to_string();
    // }

    #[test]
    fn test_hex_id() {
        // For positive numbers, should just give the smallest representation.
        // No need to zero pad.
        // https://github.com/diffblue/cbmc/blob/develop/src/util/arith_tools.cpp#L401..L424
        assert_eq!(IrepId::bitpattern_from_int(0, 4, true).to_string(), "0");
        assert_eq!(IrepId::bitpattern_from_int(12, 5, true).to_string(), "C");
        assert_eq!(IrepId::bitpattern_from_int(12, 32, true).to_string(), "C");
        assert_eq!(IrepId::bitpattern_from_int(234, 16, true).to_string(), "EA");
        assert_eq!(IrepId::bitpattern_from_int(234, 32, true).to_string(), "EA");

        // For positive numbers, signed and unsigned should produce the same value
        assert_eq!(IrepId::bitpattern_from_int(0, 4, false).to_string(), "0");
        assert_eq!(IrepId::bitpattern_from_int(12, 4, false).to_string(), "C");
        assert_eq!(IrepId::bitpattern_from_int(12, 32, false).to_string(), "C");
        assert_eq!(IrepId::bitpattern_from_int(234, 16, false).to_string(), "EA");
        assert_eq!(IrepId::bitpattern_from_int(234, 32, false).to_string(), "EA");

        // // For negative numbers, should convert to 2s complement of `width` bits, then print hex.
        assert_eq!(IrepId::bitpattern_from_int(-1, 2, true).to_string(), "3");
        assert_eq!(IrepId::bitpattern_from_int(-1, 3, true).to_string(), "7");
        assert_eq!(IrepId::bitpattern_from_int(-1, 4, true).to_string(), "F");
        assert_eq!(IrepId::bitpattern_from_int(-1, 8, true).to_string(), "FF");
        assert_eq!(IrepId::bitpattern_from_int(-1, 9, true).to_string(), "1FF");
        assert_eq!(IrepId::bitpattern_from_int(-1, 16, true).to_string(), "FFFF");
        assert_eq!(IrepId::bitpattern_from_int(-1, 32, true).to_string(), "FFFFFFFF");

        assert_eq!(IrepId::bitpattern_from_int(-12, 5, true).to_string(), "14");
        assert_eq!(IrepId::bitpattern_from_int(-12, 6, true).to_string(), "34");
        assert_eq!(IrepId::bitpattern_from_int(-12, 7, true).to_string(), "74");
        assert_eq!(IrepId::bitpattern_from_int(-12, 8, true).to_string(), "F4");
        assert_eq!(IrepId::bitpattern_from_int(-12, 32, true).to_string(), "FFFFFFF4");

        assert_eq!(IrepId::bitpattern_from_int(-127, 8, true).to_string(), "81");
        assert_eq!(IrepId::bitpattern_from_int(-127, 9, true).to_string(), "181");
        assert_eq!(IrepId::bitpattern_from_int(-127, 10, true).to_string(), "381");
        assert_eq!(IrepId::bitpattern_from_int(-127, 11, true).to_string(), "781");
        assert_eq!(IrepId::bitpattern_from_int(-127, 12, true).to_string(), "F81");
        assert_eq!(IrepId::bitpattern_from_int(-127, 36, true).to_string(), "FFFFFFF81");

        assert_eq!(IrepId::bitpattern_from_int(-255, 9, true).to_string(), "101");
        assert_eq!(IrepId::bitpattern_from_int(-255, 32, true).to_string(), "FFFFFF01");
    }
}
